In [ ]:
%%HTML
<style>
.container { width:100% }
</style>
The module extractVariables implements the function $\texttt{extractVars}(e)$ that takes a Python expression $e$ as its argument and returns the set of all variables and function names occurring in $e$.
In [ ]:
import extractVariables as ev
The function collect_variables(expr) takes a string expr that can be interpreted as a Python expression as input and collects all variables occurring in expr. It takes care to eliminate the function symbols from the names returned by extract_variables.
In [ ]:
def collect_variables(expr):
return frozenset(var for var in ev.extractVars(expr)
if var not in dir(__builtins__)
)
The function arb(S) takes a set S as input and returns an arbitrary element from
this set.
In [ ]:
def arb(S):
for x in S:
return x
Backtracking is simulated by raising the Backtrack exception. We define this new class of exceptions so that we can distinguish Backtrack exceptions from ordinary exceptions. This is done by creating a new, empty class that is derived from the class Exception.
In [ ]:
class Backtrack(Exception):
pass
Given a list of sets L, the function union(L) returns the set of all elements occurring in some set $S$ that is itself a member of the list L, i.e. we have
$$ \texttt{union}(L) = \{ x \mid \exists S \in L : x \in L \}. $$
In [ ]:
def union(L):
return { x for S in L
for x in S
}
In [ ]:
union([ {1, 2}, {'a', 'b'}, {1, 'a'} ])
The procedure solve(P) takes a constraint satisfaction problem
P as input. Here P is a triple of the form
$$ \mathcal{P} = \langle \mathtt{Variables}, \mathtt{Values}, \mathtt{Constraints} \rangle $$
where
The function solve converts the CSP P into an augmented CSP where every constraint $f$ is annotated with the variables occurring in $f$. Furthermore, the function solve maintains the following data structures:
VarsInConstrs is the set of all variables occurring in any constraint.ValuesPerVar is a dictionary mapping variables to sets of values. For every variable $x$ occurring in a constraint of P, the expression $\texttt{ValuesPerVar}(x)$ is the set of values that can be used to instantiate the variable $x$. Initially, $\texttt{ValuesPerVar}(x)$ is set to Values, but as the search for a solution proceeds, the sets $\texttt{ValuesPerVar}(x)$ are reduced by removing any values that cannot be part of a solution.Annotated is a dictionary. For every constraint f we have that Annotated[f] is the set of all variables occurring in f.UnaryConstrs is a set of pairs of the form (f, V) where f is a constraint containing only a single variable and V is the set containing just this variable.OtherConstrs is a set of pairs of the form (f, V) where f is a constraint containing more than one variable and V is the set of all variables occurring in f.Connected is a dictionary mapping variables to sets of variables. If x is a variable, then Connected[x] is the set of those variables y such that there is a constraint f that mentions both the variable x and the variable y.Var2Formulas is a dictionary mapping variables to sets of formulas. For every variable x, Var2Formulas[x] is the set of all those non-unary constraints f such that x occurs in f.The unary constraints are immediately solved. After that, the function enforce_consistency performs
consistency maintenance:
Formally, we define: A value $v$ is consistent for $x$ with respect to the constraint $f$
iff the partial assignment $\{ x \mapsto v \}$ can be extended to an assignment $A$ satisfying the constraint $f$,
i.e. for every variable $\texttt{y}_i$ occurring in f there is a value $w_i \in \texttt{ValuesPerVar}[y]$ such that
$$ \texttt{evaluate}\bigl(f, \{ x \mapsto v, y_1 \mapsto w_1, \cdots, y_n \mapsto w_n\}\bigr) = \texttt{True}. $$
The call to enforce_consistency shrinks the sets ValuesPerVars[x] until all values in ValuesPerVars[x]
are consistent with respect to all constraints.
Finally, backtrack_search is called to solve the remaining constraint satisfaction problem by the means of both backtracking and constraint propagation.
In [ ]:
def solve(P):
Variables, Values, Constraints = P
VarsInConstrs = union([ collect_variables(f) for f in Constraints ])
MisspelledVars = (VarsInConstrs - Variables) | (Variables - VarsInConstrs)
if len(MisspelledVars) > 0:
print("Did you misspell any of the following Variables?")
for v in MisspelledVars:
print(v)
ValuesPerVar = { x: Values for x in Variables }
Annotated = { f: collect_variables(f) for f in Constraints }
UnaryConstrs = { (f, V) for f, V in Annotated.items()
if len(V) == 1
}
OtherConstrs = { (f, V) for f, V in Annotated.items()
if len(V) >= 2
}
Connected = {}
Var2Formulas = variables_2_formulas(OtherConstrs)
for x in Variables:
Connected[x] = union([ V for f, V in Annotated.items()
if x in V
]) - { x }
try:
for f, V in UnaryConstrs:
var = arb(V)
ValuesPerVar[var] = solve_unary(f, var, ValuesPerVar[var])
enforce_consistency(ValuesPerVar, Var2Formulas, Annotated, Connected)
for x, Values in ValuesPerVar.items():
print(f'{x}: {Values}')
return backtrack_search({}, ValuesPerVar, OtherConstrs)
except Backtrack:
return None
The function variables_2_formulas takes the set of annotated constraints as input. It returns
a dictionary that attaches to every variable x the set of those constraints f such that x occurs in f.
In [ ]:
def variables_2_formulas(Constraints):
Dictionary = {};
for f, Vars in Constraints:
for x in Vars:
if x in Dictionary:
Dictionary[x] |= { f }
else:
Dictionary[x] = { f }
return Dictionary
The function enforce_consistency takes 4 arguments:
ValuesPerVar is a dictionary. For every variable x we have that ValuesPerVar[x] is the set of values that can be substituted for x.Var2Formulasis a dictionary. For every variable x we have that Var2Formulas[x] is the set of those formulas that mention the variable x.Annotated is a dictionary. For every constraint f, Annotated[f] is the set of variables occurring in f.Connected is a dictionary. For every variable x we have that Connected[x] is the set of those variables y that are directly connected with the variable x. Two variables x and y are directly connected if there is a constraint F such that both x and y occur in F. In this case, F is connecting x and y.
In [ ]:
def enforce_consistency(ValuesPerVar, Var2Formulas, Annotated, Connected):
UncheckedVars = set(Var2Formulas.keys())
while len(UncheckedVars) > 0:
variable = UncheckedVars.pop()
Constraints = Var2Formulas[variable]
Values = ValuesPerVar[variable]
RemovedVals = set()
for f in Constraints:
OtherVars = Annotated[f] - { variable }
for value in Values:
if not exists_values(variable, value, f, OtherVars, ValuesPerVar):
RemovedVals |= { value }
UncheckedVars |= Connected[variable]
Remaining = Values - RemovedVals
if len(Remaining) == 0:
raise Backtrack()
ValuesPerVar[variable] = Remaining
The procedure exists_values takes five arguments:
var is a variable, val is a value val, f is a constraint,Vars is the set Vars of those variables in f that are different from var, andValuesPerVar is a dictionary. For every variable x we have that ValuesPerVar[x] is the set of those values that still may be tried for x.The function checks whether there is a value for var such that the other variables occurring in the constraint f can be set to values such that the constraint f is satisfied.
In [ ]:
def exists_values(var, val, f, Vars, ValuesPerVar):
Assignments = all_assignments(Vars, ValuesPerVar)
return any(eval(f, extend(A, var, val)) for A in Assignments)
The function extend takes three arguments:
A is a dictionary,x is a variable such that A[x]is not yet defined,vis some value.It returns a new dictionary B such that B[x] = v and B[y] = A[y] for all y != x.
In [ ]:
def extend(A, x, v):
B = A.copy()
B[x] = v
return B
The function all_assignments returns the list of all possible assignments for the variables in the set Vars.
For every variable x, the values for x are taken from ValuesPerVar[x].
In [ ]:
def all_assignments(Variables, ValuesPerVar):
Variables = set(Variables) # turn frozenset into a set
if len(Variables) == 0:
return [ {} ] # list containing empty assignment
var = Variables.pop()
Values = ValuesPerVar[var]
Assignments = all_assignments(Variables, ValuesPerVar)
return [ extend(A, var, val) for A in Assignments
for val in ValuesPerVar[var]
]
In [ ]:
ValuesPerVar = { 'x': {1, 2}, 'y': {2, 3} }
Variables = { 'x', 'y' }
all_assignments(Variables, ValuesPerVar)
The function solve_unary takes a unary constraint f, a variable x and the set of values Values that can be assigned to x. It returns the subset of values that can be substituted for x such that $f[x\mapsto v]$ evaluates as True.
In [ ]:
def solve_unary(f, x, Values):
Legal = { value for value in Values
if eval(f, { x: value })
}
if len(Legal) == 0:
raise Backtrack()
return Legal
The function backtrack_search takes three arguments:
Assignment is a partial variable assignment that is represented as a
dictionary. Initially, this assignment will be the empty dictionary.backtrack_search adds the assignment of one
variable to the given assignment. ValuesPerVar is a dictionary. For every variable x, ValuesPerVar[x] is the set of values that still might be assigned to x.Constraints is a set of pairs of the form (F, V) where F is a constraint and V is the set of variables occurring in V.
In [ ]:
def backtrack_search(Assignment, ValuesPerVar, Constraints):
print(Assignment)
if len(Assignment) == len(ValuesPerVar):
return Assignment
x = most_constrained_variable(Assignment, ValuesPerVar)
for v in ValuesPerVar[x]:
try:
if is_consistent(x, v, Assignment, Constraints):
NewValues = propagate(x, v, Assignment, Constraints, ValuesPerVar)
NewAssign = Assignment.copy()
NewAssign[x] = v
return backtrack_search(NewAssign, NewValues, Constraints)
except Backtrack:
continue
raise Backtrack()
The function most_constrained_variable takes two parameters:
Assigment is a partial variable assignment that assigns values to variables. It is represented as a dictionary.ValuesPerVar is a dictionary that has variables as keys. For every variable x, ValuesPerVar[x] is the set of values that be assigned to the variable x.
The function returns an unassigned variable x such that the number of values in ValuesPerVar[x] is minimal among all other unassigned variables.
In [ ]:
def most_constrained_variable(Assignment, ValuesPerVar):
Unassigned = { (x, len(U)) for x, U in ValuesPerVar.items()
if x not in Assignment
}
minSize = min(lenU for x, lenU in Unassigned)
for x, lenU in Unassigned:
if lenU == minSize:
return x
The function propagate takes five arguments:
x is a variable,v is a value that is supposed to be assigned to x.Assignment is a partial assignment that contains assignments for variables that are different from x.Constraints is a set of annotated constraints.ValuesPerVar is a dictionary assigning sets of values to all variables. For every unassigned variable z, ValuesPerVar[z] is the set of values that still might be assigned to z.The purpose of the function propagate is to compute how the sets ValuesPerVar[z] can be shrunk when the value v is assigned to the variable x. The dictionary ValuesPerVar with appropriately reduced sets ValuesPerVar[z] is returned.
In [ ]:
def propagate(x, v, Assignment, Constraints, ValuesPerVar):
ValuesDict = ValuesPerVar.copy()
ValuesDict[x] = { v }
BoundVars = set(Assignment.keys())
for F, Vars in Constraints:
if x in Vars:
UnboundVars = Vars - BoundVars - { x }
if len(UnboundVars) == 1:
y = arb(UnboundVars)
Legal = set()
for w in ValuesDict[y]:
NewAssign = Assignment.copy()
NewAssign[x] = v
NewAssign[y] = w
if eval(F, NewAssign):
Legal.add(w)
if len(Legal) == 0:
raise Backtrack()
ValuesDict[y] = Legal
return ValuesDict
The function $\texttt{is_consistent}(\texttt{var}, \texttt{value}, \texttt{Assignment}, \texttt{csp})$ takes four arguments:
In [ ]:
def is_consistent(var, value, Assignment, Constraints):
NewAssign = Assignment.copy()
NewAssign[var] = value
return all(eval(f, NewAssign) for (f, Vs) in Constraints
if var in Vs and Vs <= NewAssign.keys()
)
In [ ]:
%run N-Queens-Problem-CSP.ipynb
In [ ]:
P = create_csp(8)
The consistency solver takes about 32 milliseconds on my desktop to solve the eight queens puzzle. Hence, for the eight queens puzzle, consistency maintenance does not help.
In [ ]:
%%time
Solution = solve(P)
print(f'Solution = {Solution}')
In [ ]:
show_solution(Solution)
In [ ]:
%run Zebra.ipynb
In [ ]:
zebra = zebra_csp()
The consistency solver takes about 37 milliseconds to solve the zebra puzzle.
In [ ]:
%%time
Solution = solve(zebra)
In [ ]:
show_solution(Solution)
In [ ]:
%run Sudoku.ipynb
In [ ]:
csp = sudoku_csp(Sudoku)
csp
In [ ]:
%%time
Solution = solve(csp)
In [ ]:
show_solution(Solution)
In [ ]:
%run Crypto-Arithmetic.ipynb
In [ ]:
csp = crypto_csp()
In [ ]:
%%time
Solution = solve(csp)
In [ ]:
show_solution(Solution)
In [ ]: